\begin{tabbing}
at src($l$):
\\[0ex]action \$a(m) 
\\[0ex]p\=recondition $P$\+
\\[0ex]sends [\$tg,$f$] on link $l$
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\oplus$(\=[@source($l$) \=precondition for "\$a"(v:$A$):\+\+
\\[0ex]$P$ State(${\it ds}$) v
\-\\[0ex]; \=sends locl("\$a")(v:$A$) on $l$:\+
\\[0ex]tagged([$\langle$"\$tg"$,\,$$\lambda$$s$,$v$. [$f$($s$,$v$)]$\rangle$],State(${\it ds}$),v):"\$tg" : $T$
\-\\[0ex]; only events in [locl("\$a")] send on $l$ with "\$tg"])
\-
\end{tabbing}